NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX
Next:List processing Up:Induction for lists Previous:Proof:

Proof:

The initial step is to show that this proposition holds for the empty list, []. From the definition of the function, rev(rev[]) = rev[] = [] as required.

Now assume that rev(revt) = t and consider h :: t.

LHS = rev(rev(h :: t))  
  = rev((revt) @ [h])     [defn of rev]
  = (rev[h]) @ (rev(revt))     [interchange law]
  = [h] @ t     [induction hypothesis and defn of rev]
  = h :: t     [defn of @]
  = RHS  
$\Box$
NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX
Next:List processing Up:Induction for lists Previous:Proof: